COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		This is a first attempt at applying circumscription induction
C00006 ENDMK
C⊗;
	This is a first attempt at applying circumscription induction
to the frame problem.  We would like to get the result that unmoved
blocks don't change their positions by applying circumscription induction
to the rule describing the change of position of a moved block.
Here is a variant that works, though it is not yet clear what reasoning
motivates the application of circumscription in precisely this way.
We have

(1)	on(x,p,move(x,p,s)).

Notice that we are writing it as a free variable formula rather than
in the form ∀x p s.on(x,p,move(x,p,s)).  What we want the circumscription
schema to express is that the only things whose position (what they are on)
can change are those whose changing follows from (1).
We write

(2)	P(y) ≡ ∃q.¬(on(y,q,move(x,p,s)) ≡ on(y,q,s))

to express that y is moved when x is moved to p.


	Choosing Q as a predicate parameter, the following formula
has the right consequences if it is taken as the circumscription formula:

(3)	Q(x) ∧ on(x,p,move(x,p,s)) ⊃ ∀y.(P(y) ⊃ Q(y)).

We need only take

(4)	Q(y) ≡ y = x

and substitute for P from (2), getting

(5)	x = x ∧ on(x,p,move(x,p,s)) ⊃ ∀y.(∃q.¬(on(y,q,move(x,p,s)) ≡ on(y,q,s))
		⊃ y = x),

which converts to

(6)	on(x,p,move(x,p,s)) ⊃ ∀y.(y ≠ x ⊃ ∀q.(on(y,q,move(x,p,s)) ≡ on(y,q,s))),

when we replace the second implication by its contrapositive.  Since the
premise of (6) is an axiom, we get

(7)	∀y.(y ≠ x ⊃ ∀q.(on(y,q,move(x,p,s)) ≡ on(y,q,s))),

which is the desired frame axiom.

	As stated above, this way of applying circumscription gives the
desired answer, but it is not clear what general principle is being
appealed to.  Applying circumscription to formulas with free variables
in them didn't come up previously.


Gluing

	Now we attempt to meet a challenge from Bob Filman to allow for
one block glued to another.  Suppose we change (1) to

(8)	on(x,p,move(x,p,s)) ∧ ∀z.(glued(z,x) ⊃ on(z,p,move(x,p,s))),

and again use the P(x) given by (2).  The circumscription induction
formula is

(9) Q(x) ∧ on(x,p,move(x,p,s)) ∧ ∀z.((¬P(z) ∨ Q(z)) ⊃ (glued(z,x) >
on(z,p,move(x,p,s)))) ⊃ ∀y.(P(y) ⊃ Q(y)).